#include <stdio.h>

/*
 * Gives an estimate of the square root.
 *
 * @name sqrtll_estimate
 * @return long long
 * @arg 0 long long
 *
 * @pre #arg0 > 0
 * @post #ret * #ret <= #arg0
 */ 
long long sqrtll_estimate (long long x) /* @dbc@ */
{
    int highest_significant_bit = 0;
    while (x > 1 << highest_significant_bit)
	++highest_significant_bit;

    return 1 << ((highest_significant_bit - 1) / 2);
}

/*
 * Calcs the sqaure root of long long integer.
 * see http://en.wikipedia.org/wiki/Methods_of_computing_square_roots
 *
 * @name sqrtll
 * @return long long
 * @arg 0 long long
 *
 * @pre #arg0 > 0
 * @post (#ret * #ret <= #arg0) && ((#ret + 1) * (#ret + 1) >= #arg0)
 */
long long sqrtll (long long x) /* @dbc@ */
{
    long long x_i = sqrtll_estimate (x);
    long x_ipp;

    while (1)
    {
	x_ipp = (x_i + x / x_i) / 2;
	if (x_ipp == x_i)
	    break;
	x_i = x_ipp;
    }

    return x_i;
}

int main (const int argc, char const* argv[])
{
    long long tests[] = {9, 16, 256, 123456, 12, 10, 20, 10000, 100000, 10000000};

    int i;

    for (i = 0; i < sizeof(tests) / sizeof (tests[0]); ++i)
	printf ("sqrtll (%lld) == %lld\n", tests[i], sqrtll (tests[i]));
    
    return 0;
}

